module ControlSystem

open Map
open Number
open Monitor
open GPS
open Bus


one sig ControlSystem { // singleton

	numbers: set Number,
	map: one Map,
	monitors : set Monitor
}

fact allNumberIntoCS{
	all l : Number | one cs : ControlSystem | l in cs.numbers
}

fact allMapIsOnlyTheControlSystemMap {
	all m : Map | all cs : ControlSystem | m = cs.map
}

fact oneBusLoneNumber{
	all b:Bus | all t:Time | lone l: Number |  b in l.buses.t
}

//Existe um monitor pra toda linha de onibus e esse monitor mostra a localizacao do proximo onibus da linha
fact monitorShowNextBus {
	all n:Number, t:Time| some m:Monitor,b:Bus| b in n.buses.t and m.show.t = b.location.t
}

fact monitorIntoCS{
	all m:Monitor | m in getMonitors[]
}

//=============>> Functions << ===================================
fun getNumbers[]: some Number{
	ControlSystem.numbers
}

fun getMap[]  : one Map {
	ControlSystem.map
}

fun getBuses[]: Bus  -> Time{
	getNumbers[].buses
}

fun getMonitors[] :  set Monitor {
	ControlSystem.monitors
}

//============>> Time operations << ==================================

// ------------------------------------ time 1 ----------------------------------------------------------

pred addBusToNumberWithTime[number:Number, b: Bus, t,t':Time]{
	b !in (number.buses).t
	(number.buses).t' = (number.buses).t + b

}

// ------------------------------------ time 2 ----------------------------------------------------------

pred changeNumberRouteWithTime[number: Number, r : Route, t,t':Time] {
	number in getNumbers[]
	r != (number.route).t
	(number.route).t' = r
}

// ------------------------------------ time 3 ----------------------------------------------------------
pred removeBusFromNumberWithTime[number : Number, b: Bus, t,t':Time] {
	number in getNumbers[]
	b in number.buses.t
	(number.buses).t' = (number.buses).t - b 
}

// ------------------------------------- time 4 --------------------------------------------------------
pred changeBusLocationWithTime[b : Bus, l:Location, t,t' : Time] {
	l != (b.location).t
	b.location.t' = l
}

----------------------------------------time 5 ----------------------------------------------------
pred monitorShowDiffLocationWithTime[m:Monitor, l:Location, t,t':Time] {
	m.show.t != l
	m.show.t' = l
}

pred init[t : Time] {
	#ControlSystem.numbers >0
}

fact traces {
	init[first]
	all pre : Time-last | let  pos = pre.next | some n : Number | some r : Route |
					some b : Bus | some l:Location| some m:Monitor|
		 removeBusFromNumberWithTime[n, b, pre,pos] or 
		 addBusToNumberWithTime[n, b, pre,pos] or
		 changeNumberRouteWithTime[n, r,pre,pos] or
		changeBusLocationWithTime[b,l,pre,pos] or
		monitorShowDiffLocationWithTime[m,l,pre,pos]
}

pred show[] {}

run show for 4 but exactly 2 Number
